0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 88 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 22 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 13 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 PiDPToQDPProof (⇒, 0 ms)
↳16 QDP
↳17 QDPOrderProof (⇔, 61 ms)
↳18 QDP
↳19 DependencyGraphProof (⇔, 0 ms)
↳20 TRUE
TRANSPOSED_IN_AG(.(X1, X2), .(X3, X4)) → U5_AG(X1, X2, X3, X4, pB_in_aggaaa(X1, X3, X4, X5, X6, X2))
TRANSPOSED_IN_AG(.(X1, X2), .(X3, X4)) → PB_IN_AGGAAA(X1, X3, X4, X5, X6, X2)
PB_IN_AGGAAA(.(X1, X2), .(X1, X3), X4, .(X3, X5), .([], X6), X7) → U2_AGGAAA(X1, X2, X3, X4, X5, X6, X7, row2colA_in_agaa(X2, X4, X5, X6))
PB_IN_AGGAAA(.(X1, X2), .(X1, X3), X4, .(X3, X5), .([], X6), X7) → ROW2COLA_IN_AGAA(X2, X4, X5, X6)
ROW2COLA_IN_AGAA(.(X1, X2), .(.(X1, X3), X4), .(X3, X5), .([], X6)) → U1_AGAA(X1, X2, X3, X4, X5, X6, row2colA_in_agaa(X2, X4, X5, X6))
ROW2COLA_IN_AGAA(.(X1, X2), .(.(X1, X3), X4), .(X3, X5), .([], X6)) → ROW2COLA_IN_AGAA(X2, X4, X5, X6)
PB_IN_AGGAAA(X1, X2, X3, .(X4, X5), X6, .(X7, X8)) → U3_AGGAAA(X1, X2, X3, X4, X5, X6, X7, X8, row2colcC_in_aggaa(X1, X2, X3, .(X4, X5), X6))
U3_AGGAAA(X1, X2, X3, X4, X5, X6, X7, X8, row2colcC_out_aggaa(X1, X2, X3, .(X4, X5), X6)) → U4_AGGAAA(X1, X2, X3, X4, X5, X6, X7, X8, pB_in_aggaaa(X7, X4, X5, X9, X10, X8))
U3_AGGAAA(X1, X2, X3, X4, X5, X6, X7, X8, row2colcC_out_aggaa(X1, X2, X3, .(X4, X5), X6)) → PB_IN_AGGAAA(X7, X4, X5, X9, X10, X8)
row2colcC_in_aggaa(.(X1, X2), .(X1, X3), X4, .(X3, X5), .([], X6)) → U11_aggaa(X1, X2, X3, X4, X5, X6, row2colcA_in_agaa(X2, X4, X5, X6))
row2colcA_in_agaa(.(X1, X2), .(.(X1, X3), X4), .(X3, X5), .([], X6)) → U7_agaa(X1, X2, X3, X4, X5, X6, row2colcA_in_agaa(X2, X4, X5, X6))
row2colcA_in_agaa([], [], [], []) → row2colcA_out_agaa([], [], [], [])
U7_agaa(X1, X2, X3, X4, X5, X6, row2colcA_out_agaa(X2, X4, X5, X6)) → row2colcA_out_agaa(.(X1, X2), .(.(X1, X3), X4), .(X3, X5), .([], X6))
U11_aggaa(X1, X2, X3, X4, X5, X6, row2colcA_out_agaa(X2, X4, X5, X6)) → row2colcC_out_aggaa(.(X1, X2), .(X1, X3), X4, .(X3, X5), .([], X6))
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
TRANSPOSED_IN_AG(.(X1, X2), .(X3, X4)) → U5_AG(X1, X2, X3, X4, pB_in_aggaaa(X1, X3, X4, X5, X6, X2))
TRANSPOSED_IN_AG(.(X1, X2), .(X3, X4)) → PB_IN_AGGAAA(X1, X3, X4, X5, X6, X2)
PB_IN_AGGAAA(.(X1, X2), .(X1, X3), X4, .(X3, X5), .([], X6), X7) → U2_AGGAAA(X1, X2, X3, X4, X5, X6, X7, row2colA_in_agaa(X2, X4, X5, X6))
PB_IN_AGGAAA(.(X1, X2), .(X1, X3), X4, .(X3, X5), .([], X6), X7) → ROW2COLA_IN_AGAA(X2, X4, X5, X6)
ROW2COLA_IN_AGAA(.(X1, X2), .(.(X1, X3), X4), .(X3, X5), .([], X6)) → U1_AGAA(X1, X2, X3, X4, X5, X6, row2colA_in_agaa(X2, X4, X5, X6))
ROW2COLA_IN_AGAA(.(X1, X2), .(.(X1, X3), X4), .(X3, X5), .([], X6)) → ROW2COLA_IN_AGAA(X2, X4, X5, X6)
PB_IN_AGGAAA(X1, X2, X3, .(X4, X5), X6, .(X7, X8)) → U3_AGGAAA(X1, X2, X3, X4, X5, X6, X7, X8, row2colcC_in_aggaa(X1, X2, X3, .(X4, X5), X6))
U3_AGGAAA(X1, X2, X3, X4, X5, X6, X7, X8, row2colcC_out_aggaa(X1, X2, X3, .(X4, X5), X6)) → U4_AGGAAA(X1, X2, X3, X4, X5, X6, X7, X8, pB_in_aggaaa(X7, X4, X5, X9, X10, X8))
U3_AGGAAA(X1, X2, X3, X4, X5, X6, X7, X8, row2colcC_out_aggaa(X1, X2, X3, .(X4, X5), X6)) → PB_IN_AGGAAA(X7, X4, X5, X9, X10, X8)
row2colcC_in_aggaa(.(X1, X2), .(X1, X3), X4, .(X3, X5), .([], X6)) → U11_aggaa(X1, X2, X3, X4, X5, X6, row2colcA_in_agaa(X2, X4, X5, X6))
row2colcA_in_agaa(.(X1, X2), .(.(X1, X3), X4), .(X3, X5), .([], X6)) → U7_agaa(X1, X2, X3, X4, X5, X6, row2colcA_in_agaa(X2, X4, X5, X6))
row2colcA_in_agaa([], [], [], []) → row2colcA_out_agaa([], [], [], [])
U7_agaa(X1, X2, X3, X4, X5, X6, row2colcA_out_agaa(X2, X4, X5, X6)) → row2colcA_out_agaa(.(X1, X2), .(.(X1, X3), X4), .(X3, X5), .([], X6))
U11_aggaa(X1, X2, X3, X4, X5, X6, row2colcA_out_agaa(X2, X4, X5, X6)) → row2colcC_out_aggaa(.(X1, X2), .(X1, X3), X4, .(X3, X5), .([], X6))
ROW2COLA_IN_AGAA(.(X1, X2), .(.(X1, X3), X4), .(X3, X5), .([], X6)) → ROW2COLA_IN_AGAA(X2, X4, X5, X6)
row2colcC_in_aggaa(.(X1, X2), .(X1, X3), X4, .(X3, X5), .([], X6)) → U11_aggaa(X1, X2, X3, X4, X5, X6, row2colcA_in_agaa(X2, X4, X5, X6))
row2colcA_in_agaa(.(X1, X2), .(.(X1, X3), X4), .(X3, X5), .([], X6)) → U7_agaa(X1, X2, X3, X4, X5, X6, row2colcA_in_agaa(X2, X4, X5, X6))
row2colcA_in_agaa([], [], [], []) → row2colcA_out_agaa([], [], [], [])
U7_agaa(X1, X2, X3, X4, X5, X6, row2colcA_out_agaa(X2, X4, X5, X6)) → row2colcA_out_agaa(.(X1, X2), .(.(X1, X3), X4), .(X3, X5), .([], X6))
U11_aggaa(X1, X2, X3, X4, X5, X6, row2colcA_out_agaa(X2, X4, X5, X6)) → row2colcC_out_aggaa(.(X1, X2), .(X1, X3), X4, .(X3, X5), .([], X6))
ROW2COLA_IN_AGAA(.(X1, X2), .(.(X1, X3), X4), .(X3, X5), .([], X6)) → ROW2COLA_IN_AGAA(X2, X4, X5, X6)
ROW2COLA_IN_AGAA(.(.(X1, X3), X4)) → ROW2COLA_IN_AGAA(X4)
From the DPs we obtained the following set of size-change graphs:
PB_IN_AGGAAA(X1, X2, X3, .(X4, X5), X6, .(X7, X8)) → U3_AGGAAA(X1, X2, X3, X4, X5, X6, X7, X8, row2colcC_in_aggaa(X1, X2, X3, .(X4, X5), X6))
U3_AGGAAA(X1, X2, X3, X4, X5, X6, X7, X8, row2colcC_out_aggaa(X1, X2, X3, .(X4, X5), X6)) → PB_IN_AGGAAA(X7, X4, X5, X9, X10, X8)
row2colcC_in_aggaa(.(X1, X2), .(X1, X3), X4, .(X3, X5), .([], X6)) → U11_aggaa(X1, X2, X3, X4, X5, X6, row2colcA_in_agaa(X2, X4, X5, X6))
row2colcA_in_agaa(.(X1, X2), .(.(X1, X3), X4), .(X3, X5), .([], X6)) → U7_agaa(X1, X2, X3, X4, X5, X6, row2colcA_in_agaa(X2, X4, X5, X6))
row2colcA_in_agaa([], [], [], []) → row2colcA_out_agaa([], [], [], [])
U7_agaa(X1, X2, X3, X4, X5, X6, row2colcA_out_agaa(X2, X4, X5, X6)) → row2colcA_out_agaa(.(X1, X2), .(.(X1, X3), X4), .(X3, X5), .([], X6))
U11_aggaa(X1, X2, X3, X4, X5, X6, row2colcA_out_agaa(X2, X4, X5, X6)) → row2colcC_out_aggaa(.(X1, X2), .(X1, X3), X4, .(X3, X5), .([], X6))
PB_IN_AGGAAA(X2, X3) → U3_AGGAAA(X2, X3, row2colcC_in_aggaa(X2, X3))
U3_AGGAAA(X2, X3, row2colcC_out_aggaa(X1, X2, X3, .(X4, X5), X6)) → PB_IN_AGGAAA(X4, X5)
row2colcC_in_aggaa(.(X1, X3), X4) → U11_aggaa(X1, X3, X4, row2colcA_in_agaa(X4))
row2colcA_in_agaa(.(.(X1, X3), X4)) → U7_agaa(X1, X3, X4, row2colcA_in_agaa(X4))
row2colcA_in_agaa([]) → row2colcA_out_agaa([], [], [], [])
U7_agaa(X1, X3, X4, row2colcA_out_agaa(X2, X4, X5, X6)) → row2colcA_out_agaa(.(X1, X2), .(.(X1, X3), X4), .(X3, X5), .([], X6))
U11_aggaa(X1, X3, X4, row2colcA_out_agaa(X2, X4, X5, X6)) → row2colcC_out_aggaa(.(X1, X2), .(X1, X3), X4, .(X3, X5), .([], X6))
row2colcC_in_aggaa(x0, x1)
row2colcA_in_agaa(x0)
U7_agaa(x0, x1, x2, x3)
U11_aggaa(x0, x1, x2, x3)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PB_IN_AGGAAA(X2, X3) → U3_AGGAAA(X2, X3, row2colcC_in_aggaa(X2, X3))
POL(.(x1, x2)) = 1 + x1 + x2
POL(PB_IN_AGGAAA(x1, x2)) = 1 + x1 + x2
POL(U11_aggaa(x1, x2, x3, x4)) = 1 + x2 + x4
POL(U3_AGGAAA(x1, x2, x3)) = x3
POL(U7_agaa(x1, x2, x3, x4)) = 1 + x2 + x4
POL([]) = 0
POL(row2colcA_in_agaa(x1)) = x1
POL(row2colcA_out_agaa(x1, x2, x3, x4)) = x3
POL(row2colcC_in_aggaa(x1, x2)) = x1 + x2
POL(row2colcC_out_aggaa(x1, x2, x3, x4, x5)) = x4
row2colcC_in_aggaa(.(X1, X3), X4) → U11_aggaa(X1, X3, X4, row2colcA_in_agaa(X4))
row2colcA_in_agaa(.(.(X1, X3), X4)) → U7_agaa(X1, X3, X4, row2colcA_in_agaa(X4))
row2colcA_in_agaa([]) → row2colcA_out_agaa([], [], [], [])
U11_aggaa(X1, X3, X4, row2colcA_out_agaa(X2, X4, X5, X6)) → row2colcC_out_aggaa(.(X1, X2), .(X1, X3), X4, .(X3, X5), .([], X6))
U7_agaa(X1, X3, X4, row2colcA_out_agaa(X2, X4, X5, X6)) → row2colcA_out_agaa(.(X1, X2), .(.(X1, X3), X4), .(X3, X5), .([], X6))
U3_AGGAAA(X2, X3, row2colcC_out_aggaa(X1, X2, X3, .(X4, X5), X6)) → PB_IN_AGGAAA(X4, X5)
row2colcC_in_aggaa(.(X1, X3), X4) → U11_aggaa(X1, X3, X4, row2colcA_in_agaa(X4))
row2colcA_in_agaa(.(.(X1, X3), X4)) → U7_agaa(X1, X3, X4, row2colcA_in_agaa(X4))
row2colcA_in_agaa([]) → row2colcA_out_agaa([], [], [], [])
U7_agaa(X1, X3, X4, row2colcA_out_agaa(X2, X4, X5, X6)) → row2colcA_out_agaa(.(X1, X2), .(.(X1, X3), X4), .(X3, X5), .([], X6))
U11_aggaa(X1, X3, X4, row2colcA_out_agaa(X2, X4, X5, X6)) → row2colcC_out_aggaa(.(X1, X2), .(X1, X3), X4, .(X3, X5), .([], X6))
row2colcC_in_aggaa(x0, x1)
row2colcA_in_agaa(x0)
U7_agaa(x0, x1, x2, x3)
U11_aggaa(x0, x1, x2, x3)